(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


Require Import FunctionalExtensionality.
Require Import Reals.
Open Scope R_scope.
Require Import Ring_theory.
Require Import Matrix.Mat.Mat_make.
Require Export Matrix.Mat.Matrix_Module.

Section lemma_needed.

Lemma fun_eq : forall (f g:R->R) ,(forall x:R,f x = g x) -> f = g.
Proof.
exact functional_extensionality.
Qed.

Definition f0  := (fun x:R => 0).
Definition f1  := (fun x:R => 1).

Definition fopp (f:R->R) := fun x => Ropp (f x).

Definition fadd (f g:R->R) := fun x => f x + g x.

Notation "f +f g" := (fadd f g) (at level 61, left associativity).

Definition fminus (f g:R->R) := fun x => f x - g x.

Notation "f -f g" := (fminus f g) (at level 61, left associativity).

Definition fmul (f g:R->R) := fun x => f x * g x.

Notation "f *f g" := (fmul f g) (at level 59, left associativity).

(** f+g = g+f **)
Lemma fun_plus_comm : forall f1 f2, f1 +f f2 = f2 +f f1.
Proof. intros. apply fun_eq. intros. unfold fadd. ring. Qed.

(** f1 + f2 + f3 = f1 + (f2 + f3) **)
Lemma fun_plus_assoc : forall f1 f2 f3, f1 +f f2 +f f3 = f1 +f ( f2 +f f3 ).
Proof. intros. apply fun_eq. intros. unfold fadd. ring. Qed.

Lemma fun_plus_assoc2: forall f1 f2 f3 f4, 
  (f1 +f f2) +f (f3 +f f4) = (f1 +f f3) +f ( f2 +f f4).
Proof. intros. apply fun_eq. intros. unfold fadd. ring. Qed.

Lemma fun_plus_zero_l : forall f , f0 +f f = f.
Proof. intros. apply fun_eq. intros. unfold fadd. unfold f0. ring. Qed.

Lemma fun_plus_zero_r : forall f , f +f f0 = f.
Proof. intros. apply fun_eq. intros. unfold fadd. unfold f0. ring. Qed.

(** f - g = - (g - f) **)
Lemma fun_minus_opp : forall f1 f2, f1 -f f2 = fopp (f2 -f f1).
Proof. intros. apply fun_eq. intros. unfold fminus. unfold fopp. ring. Qed.

(** f1-f2-f3 = f1-(f2+f3) **)
Lemma fun_minus_assoc : forall f1 f2 f3 , f1 -f f2 -f f3 = f1 -f (f2 +f f3).
Proof. intros. apply fun_eq. intros. unfold fminus. unfold fadd. ring. Qed.

Lemma fun_minus_assoc2 : forall f1 f2 f3 f4,
   (f1 +f f2) -f (f3 +f f4) = (f1 -f f3) +f (f2 -f f4).
Proof. intros. apply fun_eq. intros. unfold fminus. unfold fadd. ring. Qed.

Lemma fun_minus_zero_l : forall f , f0 -f f = fopp f.
Proof. intros. apply fun_eq. intros. unfold fminus,fopp. unfold f0. ring. Qed.

Lemma fun_minus_zero_r : forall f , f -f f0 = f.
Proof. intros. apply fun_eq. intros. unfold fminus. unfold f0. ring. Qed.

Lemma fun_minus_self:forall f , f -f f = f0.
Proof. intros. apply fun_eq. intros. unfold fminus. unfold f0. ring. Qed.

Lemma fun_mult_add_distr_l : forall a b c , (a +f b) *f c = (a *f c) +f (b *f c).
Proof. intros. unfold fadd. unfold fmul. apply fun_eq. intros. ring. Qed.

Lemma fun_mult_add_distr_r : forall a b c , a *f (b +f c)  = (a *f b) +f (a *f c).
Proof. intros. unfold fadd. unfold fmul. apply fun_eq. intros. ring. Qed.

Lemma fun_mult_sub_distr_l : forall a b c , (a -f b) *f c = (a *f c) -f (b *f c).
Proof. intros. unfold fminus. unfold fmul. apply fun_eq. intros. ring. Qed.

Lemma fun_mult_sub_distr_r : forall a b c , a *f (b -f c)  = (a *f b) -f (a *f c).
Proof. intros. unfold fminus. unfold fmul. apply fun_eq. intros. ring. Qed.

Lemma fun_mult_zero_l : forall f , f0 *f f = f0.
Proof. intros. apply fun_eq. intros. unfold fmul. unfold f0. ring. Qed.

Lemma fun_mult_zero_r : forall f , f *f f0 = f0.
Proof. intros. apply fun_eq. intros. unfold fmul. unfold f0. ring. Qed.

Lemma fun_mult_one_l : forall f , f1 *f f = f.
Proof. intros. apply fun_eq. intros. unfold fmul. unfold f1. ring. Qed.

Lemma fun_mult_one_r : forall f , f *f f1 = f.
Proof. intros. apply fun_eq. intros. unfold fmul. unfold f1. ring. Qed.

(** f*g = g*f **)
Lemma fun_mult_comm : forall f g, f *f g = g *f f.
Proof. intros. apply fun_eq. intros. unfold fmul. ring. Qed.

(** f1 * f2 * f3 = f1 * (f2 * f3) **)
Lemma fun_mult_assoc : forall f1 f2 f3, f1 *f f2 *f f3 = f1 *f (f2 *f f3).
Proof. intros. apply fun_eq. intros. unfold fmul. ring. Qed.

End lemma_needed.

Module FM.
Definition A := R->R.

Definition One := f1.
Definition Zero := f0.

Definition opp := fopp.
Definition add := fadd.
Definition sub := fminus.
Definition mul := fmul.

Definition add_comm := fun_plus_comm.
Definition add_assoc := fun_plus_assoc.
Definition add_zero_l := fun_plus_zero_l.
Definition add_zero_r := fun_plus_zero_r.

Definition add_assoc2 := fun_plus_assoc2.
Definition sub_assoc := fun_minus_assoc.
Definition sub_assoc2:= fun_minus_assoc2.
Definition sub_opp := fun_minus_opp.
Definition sub_zero_l:= fun_minus_zero_l.
Definition sub_zero_r:= fun_minus_zero_r.
Definition sub_self:= fun_minus_self.

Definition mul_add_distr_l:= fun_mult_add_distr_l.
Definition mul_add_distr_r := fun_mult_add_distr_r.
Definition mul_sub_distr_l := fun_mult_sub_distr_l.
Definition mul_sub_distr_r := fun_mult_sub_distr_r.
Definition mul_assoc := fun_mult_assoc.
Definition mul_zero_l := fun_mult_zero_l.
Definition mul_zero_r := fun_mult_zero_r.
Definition mul_one_l:= fun_mult_one_l.
Definition mul_one_r:= fun_mult_one_r.
Definition mul_comm := fun_mult_comm.

End FM.

Module FMatrix := Matrix(FM).

Definition FMtrans := @FMatrix.Mtrans.
Arguments FMtrans {m} {n}.

Definition FMadd := @FMatrix.Madd.
Arguments FMadd {m} {n}.

Definition FMsub := @FMatrix.Msub.
Arguments FMsub {m} {n}.

Definition FMopp := @FMatrix.Mopp.
Arguments FMopp {m} {n}.

Definition FMmul := @FMatrix.Mmul.
Arguments FMmul {m} {n} {p}.

Definition FMmulc_l := @FMatrix.Mmulc_l.
Arguments FMmulc_l {m} {n}.

Definition FMmulc_r := @FMatrix.Mmulc_r.
Arguments FMmulc_r {m} {n}.

Definition FMO := @FMatrix.MO.

Definition FMI := @FMatrix.MI.

Notation "m1 FM+ m2" := (FMadd m1 m2) (at level 65).

Notation "m1 FM- m2" := (FMsub m1 m2) (at level 65).

Notation " FM- m" := (FMopp m) (at level 65).

Notation "m1 FM* m2" := (FMmul m1 m2) (at level 60).

Notation "c FF* m" := (FMmulc_l c m) (at level 60).

Notation "m *FF c" := (FMmulc_r m c) (at level 60).

(*Definition FMeq_visit := @FMatrix.Meq_visit.
Arguments FMeq_visit {m} {n}. *)

Definition FMadd_comm := @FMatrix.Madd_comm.
Arguments FMadd_comm {m} {n}.

Definition FMadd_assoc := @FMatrix.Madd_assoc.
Arguments FMadd_assoc {m} {n}.

Definition FMadd_zero_l := @FMatrix.Madd_zero_l.
Arguments FMadd_zero_l {m} {n}.

Definition FMadd_zero_r := @FMatrix.Madd_zero_r.
Arguments FMadd_zero_r {m} {n}.

Definition FMsub_comm := @FMatrix.Msub_comm.
Arguments FMsub_comm {m} {n}.

Definition FMsub_assoc := @FMatrix.Msub_assoc.
Arguments FMsub_assoc {m} {n}.

Definition FMsub_O_l := @FMatrix.Msub_O_l.
Arguments FMsub_O_l {m} {n}.

Definition FMsub_O_r := @FMatrix.Msub_O_r.
Arguments FMsub_O_r {m} {n}.

Definition FMsub_self := @FMatrix.Msub_self.
Arguments FMsub_self {m} {n}.

Definition FMmul_distr := @FMatrix.Mmul_add_distr_l.
Arguments FMmul_distr {m} {n}.

Definition FMmul_assoc:= @FMatrix.Mmul_assoc.
Arguments FMmul_assoc {m} {n} {p} {k}.

Definition FMmul_zero_l:=@FMatrix.Mmul_zero_l.
Arguments FMmul_zero_l {m} {n}.

Definition FMmul_zero_r:=@FMatrix.Mmul_zero_r.
Arguments FMmul_zero_r {m}{n}.

Definition FMmul_mul_unit_l := @FMatrix.Mmul_unit_l.
Arguments FMmul_mul_unit_l {m} {n}.

Definition FMmul_mul_unit_r := @FMatrix.Mmul_unit_r.
Arguments FMmul_mul_unit_r {m} {n}.

Definition FMmulc_comm := @FMatrix.Mmulc_comm.
Arguments FMmulc_comm {m} {n}.

Definition FMmulc_distr_l :=@FMatrix.Mmulc_distr_l.
Arguments FMmulc_distr_l {m} {n}.

Definition FMmulc_0_l:=@FMatrix.Mmulc_0_l.
Arguments FMmulc_0_l {m} {n}.

Definition FMtteq := @FMatrix.Mtteq.
Arguments FMtteq {m} {n}.

Definition FMcteq := @FMatrix.Mcteq.
Arguments FMcteq {m} {n}.

Definition FMteq_add := @FMatrix.Mteq_add.
Arguments FMteq_add {m} {n}.

Definition FMteq_sub := @FMatrix.Mteq_sub.
Arguments FMteq_sub {m} {n}.

Definition FMteq_mul := @FMatrix.Mteq_mul.
Arguments FMteq_mul {m} {n}.

Definition FMtrans_MI:= @FMatrix.Mtrans_MI.
Arguments FMtrans_MI {n}.

Require Export Setoid.
Require Export Relation_Definitions.
Set Implicit Arguments.

Add Parametric Relation {m n:nat} : (Mat (R->R) m n) (@M_eq (R->R) m n) 
  reflexivity proved by (@Meq_ref (R->R) m n)
  symmetry proved by (@Meq_sym (R->R) m n)
  transitivity proved by (@Meq_trans (R->R) m n)
  as FMeq_rel.


Lemma Fmat_add_compat : 
  forall m n, 
     forall x x' : (Mat (R->R) m n ), @M_eq (R->R) m n x x' ->
     forall y y' : (Mat (R->R) m n ), @M_eq (R->R) m n y y'->
        @M_eq (R->R) m n (FMadd x y) (FMadd x' y').
Proof.
  intros.
  unfold FMadd,FMatrix.Madd. rewrite H,H0.
  reflexivity.
Qed.

Add Parametric Morphism {m n :nat}:(@FMadd m n)
  with signature (@M_eq (R->R) m n) ==> 
  (@M_eq (R->R) m n) ==> (@M_eq (R->R) m n) 
  as Fmat_add_mor.
Proof.
exact (@Fmat_add_compat m n).
Qed.

Lemma Fmat_sub_compat : 
  forall m n, 
     forall x x' : (Mat (R->R) m n ), @M_eq (R->R) m n x x' ->
     forall y y' : (Mat (R->R) m n ), @M_eq (R->R) m n y y'->
        @M_eq (R->R) m n (FMsub x y) (FMsub x' y').
Proof.
  intros.
  unfold FMsub,FMatrix.Msub. rewrite H,H0.
  reflexivity.
Qed.

Add Parametric Morphism {m n :nat}:(@FMsub m n)
  with signature (@M_eq (R->R) m n) 
    ==> (@M_eq (R->R) m n) ==> (@M_eq (R->R) m n) 
  as Fmat_sub_mor.
Proof.
exact (@Fmat_sub_compat m n).
Qed.

Lemma Fmat_opp_compat : 
  forall m n, 
     forall x x' : (Mat (R->R) m n ), @M_eq (R->R) m n x x' ->
        @M_eq (R->R) m n (FMopp x ) (FMopp x' ).
Proof.
  intros.
  unfold FMopp,FMatrix.Mopp. rewrite H.
  reflexivity.
Qed.

Add Parametric Morphism {m n :nat}:(@FMopp m n)
  with signature (@M_eq (R->R) m n) ==> (@M_eq (R->R) m n)
  as Fmat_opp_mor.
Proof.
exact (@Fmat_opp_compat m n).
Qed.

Lemma Fmat_trans_compat : 
  forall m n, 
     forall x x' : (Mat (R->R) m n ), @M_eq (R->R) m n x x' ->
        @M_eq (R->R) n m (FMtrans x ) (FMtrans x' ).
Proof.
  intros.
  unfold FMtrans,FMatrix.Mtrans. rewrite H.
  reflexivity.
Qed.

Add Parametric Morphism {m n :nat}:(@FMtrans m n)
  with signature (@M_eq (R->R) m n) ==> (@M_eq (R->R) n m)
  as Fmat_trans_mor.
Proof.
exact (@Fmat_trans_compat m n).
Qed.

Lemma Fmat_mul_compat : 
  forall m n p, 
     forall x x' : (Mat (R->R) m n ), @M_eq (R->R) m n x x' ->
     forall y y' : (Mat (R->R) n p ), @M_eq (R->R) n p y y'->
        @M_eq (R->R) m p (FMmul x y) (FMmul x' y').
Proof.
  intros.
  unfold FMmul,FMatrix.Mmul. rewrite H,H0.
  reflexivity.
Qed.

Add Parametric Morphism {m n p :nat}:(@FMmul m n p)
  with signature (@M_eq (R->R) m n) 
    ==> (@M_eq (R->R) n p) ==> (@M_eq (R->R) m p) 
  as Fmat_mul_mor.
Proof.
exact (@Fmat_mul_compat m n p).
Qed.







